<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Maths in lean : Linear Algebra</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="maths-in-lean--linear-algebra" class="markdown-heading">Maths in lean : Linear Algebra <a class="hover-link" href="#maths-in-lean--linear-algebra">#</a></h1>
<h3 id="semimodules-modules-and-vector-spaces" class="markdown-heading">Semimodules, Modules and Vector Spaces <a class="hover-link" href="#semimodules-modules-and-vector-spaces">#</a></h3>
<h4 id="a-hrefhttpsleanprover-communitygithubiomathlib_docsalgebramodulehtmlcodealgebramodulecodea" class="markdown-heading"><a href="https://leanprover-community.github.io/mathlib_docs/algebra/module.html"><code>algebra.module</code></a> <a class="hover-link" href="#a-hrefhttpsleanprover-communitygithubiomathlib_docsalgebramodulehtmlcodealgebramodulecodea">#</a></h4>
<p>This file defines the typeclass <code>semimodule R M</code>, which gives an <code>R</code>-semimodule structure on the type <code>M</code>, and similarly <code>module R M</code> and <code>vector_space R M</code>.
An additive commutative monoid <code>M</code> is a semimodule over the semiring <code>R</code> if there is a scalar multiplication <code>•</code> (<code>has_scalar.smul</code>) that satisfies the expected distributivity axioms for <code>+</code> (in <code>M</code> and <code>R</code>) and <code>*</code> (in <code>R</code>).
To define a <code>semimodule R M</code> instance, you first need instances for <code>semiring R</code> and <code>add_comm_monoid M</code>.
By splitting out these dependencies, we avoid instance loops and diamonds.</p>
<p>A module (typeclass <code>module</code>) is a semimodule that additionally requires that <code>R</code> is a ring and <code>M</code> is a group.
A vector space (typeclass <code>vector_space</code>) is a module that additionally requires that <code>R</code> is a field.
All vector spaces are also modules, and all modules are also semimodules.</p>
<p>Let <code>m</code> be an arbitrary type, e.g. <code>fin n</code>, then the typical examples are:
<code>m → ℕ</code> is an <code>ℕ</code>-semimodule, <code>m → ℤ</code> is a <code>ℤ</code>-module and <code>m → ℚ</code> is a <code>ℚ</code>-vector space
(outside of type theory, these are known as <code>ℕ^m</code>, <code>ℤ^m</code> and <code>ℚ^m</code> respectively).
These instances are defined in <a href="https://leanprover-community.github.io/mathlib_docs/algebra/pi_instances.html"><code>algebra.pi_instances</code></a>.
A (semi)ring is a (semi)module over itself, with <code>•</code> defined as <code>*</code> (this equality is stated by the <code>simp</code> lemma <a href="https://leanprover-community.github.io/mathlib_docs/algebra/module.html#smul_eq_mul"><code>smul_eq_mul</code></a>).</p>
<p>The file <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html"><code>linear_algebra.basis</code></a> defines linear independence and bases for modules.</p>
<p>The file <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/dimension.html"><code>linear_algebra.dimension</code></a> defines the dimension of a vector space as the minimum cardinality of a basis.
The <code>rank</code> of a linear map is defined as the dimension of its image.
Most definitions in this file are non-computable.</p>
<h3 id="matrices" class="markdown-heading">Matrices <a class="hover-link" href="#matrices">#</a></h3>
<h4 id="a-hrefhttpsleanprover-communitygithubiomathlib_docsdatamatrixbasichtmlcodedatamatrixbasiccodea" class="markdown-heading"><a href="https://leanprover-community.github.io/mathlib_docs/data/matrix/basic.html"><code>data.matrix.basic</code></a> <a class="hover-link" href="#a-hrefhttpsleanprover-communitygithubiomathlib_docsdatamatrixbasichtmlcodedatamatrixbasiccodea">#</a></h4>
<p>The type <code>matrix m n α</code> contains rectangular, <code>m</code> by <code>n</code> arrays of elements of the type <code>α</code>.
It is an alias for the type <code>m → n → α</code>, under the assumptions <code>[fintype m] [fintype n]</code> stating that <code>m</code> and <code>n</code> have finitely many elements.
A matrix type can be indexed over arbitrary <code>fintype</code>s.
For example, the adjacency matrix of a graph could be indexed over the nodes in that graph.
If you want to specify the dimensions of a matrix as natural numbers <code>m n : ℕ</code>, you can use <code>fin m</code> and <code>fin n</code> as index types.</p>
<p>A matrix is constructed by giving the map from indices to entries: <code>(λ (i : m) (j : n), (_ : α)) : matrix m n α</code>.
For matrices indexed by natural numbers, you can also use the notation defined in <a href="https://leanprover-community.github.io/mathlib_docs/data/matrix/notation.html"><code>data.matrix.notation</code></a>: <code>![![a, b, c], ![b, c, d]] : matrix (fin 2) (fin 3) α</code>.
To get an entry of the matrix <code>M : matrix m n α</code> at row <code>i : m</code> and column <code>j : n</code>,
you can apply <code>M</code> to the indices: <code>M i j : α</code>.
Lemmas about the entries of a matrix typically end in <code>_val</code>: <code>add_val M N i j : (M + N) i j = M i j + N i j</code>.</p>
<p>Matrix multiplication and transpose have notation that is made available by the command <code>open_locale matrix</code>.
The infix operator <code>⬝</code> stands for <code>matrix.mul</code>,
and a postfix operator <code>ᵀ</code> stands for <code>matrix.transpose</code>.</p>
<p>When working with matrices, a <em>vector</em> means a function <code>m → α</code> for an arbitrary <code>fintype</code> <code>m</code>.
These have a module (or vector space) structure defined in <a href="https://leanprover-community.github.io/mathlib_docs/algebra/pi_instances.html"><code>algebra.pi_instances</code></a>
consisting of pointwise addition and multiplication.
The distinction between row and column vectors is only made by the choice of function.
For example, <code>mul_vec M v</code> multiplies a matrix with a column vector <code>v : m → α</code> and <code>vec_mul v M</code> multiplies a row vector <code>v : m → α</code> with a matrix.
If you use <code>mul_vec</code> and <code>vec_mul</code> a lot, you might want to consider using a linear map instead (see below).</p>
<p>Permutation matrices are defined in <a href="https://leanprover-community.github.io/mathlib_docs/data/matrix/pequiv.html"><code>data.matrix.pequiv</code></a>.</p>
<p>The determinant of a matrix is defined in <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/determinant.html"><code>linear_algebra.determinant</code></a>.</p>
<p>The adjugate and for nonsingular matrices, the inverse is defined in <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/nonsingular_inverse.html"><code>linear_algebra.nonsingular_inverse</code></a>.</p>
<p>The type <code>special_linear_group m R</code> is the group of <code>m</code> by <code>m</code> matrices with determinant <code>1</code>,
and is defined in <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/special_linear_group.html"><code>linear_algebra.special_linear_group</code></a>.</p>
<h3 id="linear-maps-and-equivalences" class="markdown-heading">Linear Maps and Equivalences <a class="hover-link" href="#linear-maps-and-equivalences">#</a></h3>
<h4 id="a-hrefhttpsleanprover-communitygithubiomathlib_docslinear_algebrabasichtmlcodelinear_algebrabasiccodea" class="markdown-heading"><a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html"><code>linear_algebra.basic</code></a> <a class="hover-link" href="#a-hrefhttpsleanprover-communitygithubiomathlib_docslinear_algebrabasichtmlcodelinear_algebrabasiccodea">#</a></h4>
<p>The type <code>M →[R]ₗ M₂</code>, or <code>linear_map R M M₂</code>, represents <code>R</code>-linear maps from the <code>R</code>-module <code>M</code> to the <code>R</code>-mdule <code>M₂</code>.
These are defined by their action on elements of <code>M</code>.
The type <code>M ≃[R]ₗ M₂</code>, or <code>linear_equiv R M M₂</code>, is the type of invertible <code>R</code>-linear maps from <code>M</code> to <code>M₂</code>.</p>
<p>The equivalence between matrices and linear maps is formalised in <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix.html"><code>linear_algebra.matrix</code></a>.
<a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/matrix.html#linear_equiv_matrix%27"><code>linear_equiv_matrix&#x27;</code></a> shows that <code>matrix.mul_vec</code> is a linear equivalence between <code>matrix m n R</code> and <code>(n → R) →[R]ₗ (m → R)</code>.
In addition, <code>linear_equiv_matrix</code> takes a basis <code>ι</code> for <code>M₁</code> and <code>κ</code> for <code>M₂</code>
and gives the equivalence between <code>R</code>-linear maps between <code>M₁</code> and <code>M₂</code> and <code>matrix ι κ R</code>.
If you have an explicit basis for your maps, this equivalence allows you to do calculations such as getting the determinant.</p>
<p>The difference between matrices and linear maps is that matrices are in their essence an array of entries
(which incidentally allows actions such as <code>matrix.mul_vec</code>),
while linear maps are in their essence an action on vectors
(which incidentally can be represented by a matrix if we have a finite basis).
If you want to do computations, a matrix is a better choice.
If you want to do proofs without computations, a linear map is a better choice.</p>
<p>The type <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.general_linear_group"><code>general_linear_group R M</code></a> is the group of invertible <code>R</code>-linear maps from <code>M</code> to itself.
<code>general_linear_equiv R M</code> is the equivalence between <code>general_linear_group</code> and <code>M ≃[R]ₗ M</code>.
<code>special_linear_group.to_GL</code> is the embedding from the special linear group (of matrices) to the general linear group (of linear maps).</p>
<p>The dual space, consisting of linear maps <code>M →[R]ₗ R</code>, is defined in <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/dual.html"><code>linear_algebra.dual</code></a>.</p>
<h3 id="bilinear-sesquilinear-and-quadratic-forms" class="markdown-heading">Bilinear, Sesquilinear and Quadratic Forms <a class="hover-link" href="#bilinear-sesquilinear-and-quadratic-forms">#</a></h3>
<h4 id="a-hrefhttpsleanprover-communitygithubiomathlib_docslinear_algebrabilinear_formhtmlcodelinear_algebrabilinear_formcodea" class="markdown-heading"><a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html"><code>linear_algebra.bilinear_form</code></a> <a class="hover-link" href="#a-hrefhttpsleanprover-communitygithubiomathlib_docslinear_algebrabilinear_formhtmlcodelinear_algebrabilinear_formcodea">#</a></h4>
<p>For an <code>R</code>-module <code>M</code>, the type <code>bilin_form R M</code> is the type of maps <code>M → M → R</code> that are linear in both arguments.
The equivalence between <code>bilin_form R M</code> and maps <code>M →ₗ[R] M →ₗ[R] R</code> that are linear in both arguments is called <code>bilin_linear_map_equiv</code>.
A matrix <code>M</code> corresponds to a bilinear form that maps vectors <code>v</code> and <code>w</code> to <code>row v ⬝ M ⬝ col w</code>.
The equivalence between <code>bilin_form R (n → R)</code> and <code>matrix n n R</code> is called <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form_equiv_matrix"><code>bilin_form_equiv_matrix</code></a>.</p>
<h4 id="a-hrefhttpsleanprover-communitygithubiomathlib_docslinear_algebrasesquilinear_formhtmlcodelinear_algebrasesquilinear_formcodea" class="markdown-heading"><a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/sesquilinear_form.html"><code>linear_algebra.sesquilinear_form</code></a> <a class="hover-link" href="#a-hrefhttpsleanprover-communitygithubiomathlib_docslinear_algebrasesquilinear_formhtmlcodelinear_algebrasesquilinear_formcodea">#</a></h4>
<p>For an <code>R</code>-module <code>M</code> and <code>I : ring_anti_equiv R R</code>, the type <code>sesq_form R M I</code> is the type of maps <code>M → M → R</code> that are linear in the first argument and that in the second argument are antilinear with respect to an <code>R</code>-<a href="https://leanprover-community.github.io/mathlib_docs/ring_theory/maps.html#ring_anti_equiv">antiautomorphism</a> <code>I</code>.
Antilinearity of <code>f</code> with respect to a ring antiautomorphism <code>I</code> means the following equations hold: <code>f x (a • y) = I a * f x y</code>, <code>I 1 = 1</code>, <code>I (x + y) = I x + I y</code> and <code>I (x * y) = I y * I x</code>.</p>
<h4 id="a-hrefhttpsleanprover-communitygithubiomathlib_docslinear_algebraquadratic_formhtmlcodelinear_algebraquadratic_formcodea" class="markdown-heading"><a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html"><code>linear_algebra.quadratic_form</code></a> <a class="hover-link" href="#a-hrefhttpsleanprover-communitygithubiomathlib_docslinear_algebraquadratic_formhtmlcodelinear_algebraquadratic_formcodea">#</a></h4>
<p>For an <code>R</code>-module <code>M</code>, the type <code>quadratic_form R M</code> is the type of maps <code>f : M → R</code> such that <code>f (a • x) = a * a * f x</code> and <code>λ x y, f (x + y) - f x - f y</code> is a bilinear map.</p>
<p>Up to a factor <code>2</code>, the theory of quadratic and bilinear forms is equivalent.
<a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#bilin_form.to_quadratic_form"><code>bilin_form.to_quadratic_form f</code></a> is the quadratic form given by <code>λ x, f x x</code>.
<a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#quadratic_form.associated"><code>quadratic_form.associated f</code></a> is the bilinear form given by <code>λ x y, ⅟2 * (f (x + y) - f x - f y)</code> (if there is a multiplicative inverse of <code>2</code>).
<a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#quadratic_form.to_matrix"><code>quadratic_form.to_matrix</code></a> and <a href="https://leanprover-community.github.io/mathlib_docs/linear_algebra/quadratic_form.html#matrix.to_quadratic_form"><code>matrix.to_quadratic_form</code></a> are the maps between quadratic forms and matrices.</p>

  </div>
</div>

  <nav class="footer navbar navbar-expand-lg navbar-light bg-light justify-content-end">
  <ul class="nav">
    <li class="nav-item">
      <a class="nav-link active" href="https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/theories/linear_algebra.md">Suggest edits to this page on GitHub</a>
    </li>
  </ul>
</nav>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>